(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun ae () Real)
(declare-fun o () Real)
(declare-fun af () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun ag () Real)
(declare-fun s () Real)
(declare-fun ah () Real)
(declare-fun t () Real)
(declare-fun ai () Real)
(declare-fun u () Real)
(declare-fun v () Real)
(declare-fun w () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun aj () Real)
(declare-fun ak () Real)
(declare-fun al () Real)
(declare-fun vuscore2dollarskuscore97_shifted () Real)
(declare-fun am () Real)
(declare-fun an () Real)
(declare-fun ao () Real)
(declare-fun ap () Real)
(declare-fun aq () Real)
(declare-fun ar () Real)
(declare-fun v_shifted () Real)
(declare-fun V_shifted () Real)
(declare-fun I1uscore2dollarskuscore89_shifted () Real)
(declare-fun ep_shifted () Real)
(declare-fun ts7uscore2_shifted () Real)
(declare-fun x_shifted () Real)
(assert (exists ((af Real)) (= (and (< (+ (/ (* (- a an)) (* (- f ar))) w (/ ab 0)) af) (xor true (<= ts7uscore2_shifted aq 0.0 (+ (* ao ts7uscore2_shifted) (- d q))) (= 0 ah)) (< (* (+ (+ (* (- d q) (+ (* (* (- n ak)) (- h v))))) (* (* ao (- h v)) (+ (* (- h v)) (* (- d q)))))) 0.0) (<= v_shifted 0.0 ao) (< 0.0 (- h v))) (< (+ (/ (* (+ (* ao aq) (- d q)) (+ (* ao aq) (- d q))) (* (- n ak)))) aj))))
(assert (= o b af c p vuscore2dollarskuscore97_shifted aa r x_shifted e ag s ac t ad ai g u i (+ w ts7uscore2_shifted)))
(assert (= j x V_shifted k y I1uscore2dollarskuscore89_shifted l z ep_shifted m aj n (+ ak ap) ae al am))
(check-sat)
